|
In logic, linear temporal logic or linear-time temporal logic〔Logic in Computer Science: Modelling and Reasoning about Systems: page 175〕〔(Linear-time Temporal Logic )〕 (LTL) is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths, e.g., a condition will eventually be true, a condition will be true until another fact becomes true, etc. It is a fragment of the more complex CTL *, which additionally allows branching time and quantifiers. Subsequently LTL is sometimes called ''propositional temporal logic'', abbreviated ''PTL''. Linear temporal logic (LTL) is a fragment of S1S. LTL was first proposed for the formal verification of computer programs by Amir Pnueli in 1977.〔Amir Pnueli, The temporal logic of programs. ''Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS)'', 1977, 46–57. 〕 ==Syntax== LTL is built up from a finite set of propositional variables ''AP'', the logical operators ¬ and ∨, and the temporal modal operators X (some literature uses O or N) and U. Formally, the set of LTL formulas over ''AP'' is inductively defined as follows: * if p ∈ ''AP'' then p is an LTL formula; * if ψ and φ are LTL formulas then ¬ψ, φ ∨ ψ, X ψ, and φ U ψ are LTL formulas.〔Sec. 5.1 of Christel Baier and Joost-Pieter Katoen, Principles of Model Checking, MIT Press ()〕 X is read as next and U is read as until. Other than these fundamental operators, there are additional logical and temporal operators defined in terms of the fundamental operators to write LTL formulas succinctly. The additional logical operators are ∧, →, ↔, true, and false. Following are the additional temporal operators. *G for always (globally) *F for eventually (in the future) *R for release *W for weakly until 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Linear temporal logic」の詳細全文を読む スポンサード リンク
|